We want to prove that given two intervals \mbox{$(<S_{1}, \vec{i}>,
  <S_{2}, \vec{i'}>)$} and \mbox{$(<S_{3}, \vec{j}>, <S_{4},
  \vec{j'}>)$} that do not interfere, then tiling statements
$S_1$,\ldots,$S_4$ at depths where the FCO property on data-flow dependences 
holds preserves the non-interference of the two intervals. 

The goal of this section is to show (although this may be trivial) that
we can apply tiling on loop bands that verify the FCO property for 
data-flow dependences while ignoring false dependences.

Loop tiling is composed of two simple loop transformations: loop
strip-mining and loop interchange.  Strip-mining is always possible
and does not impact the ordering of statement instances, hence it does
not impact live range interference.

Let us now prove that applying loop interchange preserves the
non-interference condition.  Let $\preceq$ denote the product
ordering defined as follows :
$$\textit (a,b) \preceq (c,d) \Leftrightarrow a \le c~and~b \le d.$$


The FCO property on data-flow dependences gaurantees that $$\vec{i}
\ll \vec{i'} \quad\wedge\quad \vec{j} \ll \vec{j'}$$ The
non-interference of the two intervals applied at all depths guarantees
that 
$$\vec{i'} \preceq \vec{j}
\quad\vee\quad
\vec{j'} \preceq \vec{i}$$
We conclude that
$$\vec{i} \ll\vec{i'} \preceq \vec{j} \ll \vec{j'}
\quad\vee\quad
\vec{j} \ll \vec{j'} \preceq \vec{i} \ll \vec{i'}$$
Let's consider the case $\vec{i} \ll\vec{i'} \preceq \vec{j} \ll \vec{j'}$. We have:

 \begin{equation}
 \begin{pmatrix}
 	...\\
 	i_{k1} \\
 	... \\
 	i_{k2} \\
 	...
  \end{pmatrix}
 \ll
 \begin{pmatrix}
 	...\\
 	i'_{k1} \\
 	... \\
 	i'_{k2} \\
 	...
  \end{pmatrix}
 \preceq
  \begin{pmatrix}
 	...\\
 	j_{k1} \\
 	... \\
 	j_{k2} \\
 	...
  \end{pmatrix}
 \ll
 \begin{pmatrix}
 	...\\
 	j'_{k1} \\
 	... \\
 	j'_{k2} \\
 	...
  \end{pmatrix}
 \label{eq:non_interference_iterator_vector_relation}
 \end{equation}



% We want to verify that if the order $\vec{i} \preceq \vec{i'} \preceq \vec{j}  \preceq \vec{j'}$ is assured before tiling, this order is
% preserved after tiling (and similarly for $\vec{j} \preceq \vec{j'} \preceq \vec{i} \preceq \vec{i'}$).

% Given $i_{1}, i_{2}$ the values of two dimensions in the iterator vector $\vec{i'}$ (resp. $j_{1}, j_{2}$ for $\vec{j}$).
% $\vec{i} \preceq \vec{i'} \preceq \vec{j} \preceq \vec{j'} $ is true if (\ref{eq:non_interference_iterator_vector_relation}) is true.
% \begin{equation}
% \begin{pmatrix}
% 	...\\
% 	i_{1} \\
% 	... \\
% 	i_{2} \\
% 	...
%  \end{pmatrix}
% \preceq
% \begin{pmatrix}
% 	...\\
% 	i'_{1} \\
% 	... \\
% 	i'_{2} \\
% 	...
%  \end{pmatrix}
% \preceq
%  \begin{pmatrix}
% 	...\\
% 	j_{1} \\
% 	... \\
% 	j_{2} \\
% 	...
%  \end{pmatrix}
% \preceq
% \begin{pmatrix}
% 	...\\
% 	j'_{1} \\
% 	... \\
% 	j'_{2} \\
% 	...
%  \end{pmatrix}
% \label{eq:non_interference_iterator_vector_relation}
% \end{equation}

% i.e. if (\ref{eq:equation_to_be_preserved_after_tiling}) is true. 
% \begin{equation}
% i'_{1} \leq j_{1} ~ and ~ i'_{2} \leq j_{2} 
% \label{eq:equation_to_be_preserved_after_tiling}
% \end{equation}

% Our goal is to show that (\ref{eq:equation_to_be_preserved_after_tiling})
% is preserved when tiling is applied.

Loop interchange at depths $k_1$ and $k_2$ is defined as follows:
$$\theta_{\textrm{interchange}} \begin{pmatrix}
  ...\\
  i_{k_1} \\
  ... \\
  i_{k_2} \\
  ...
\end{pmatrix} = 
\begin{pmatrix}
  ...\\
  i_{k_2} \\
  ... \\
  i_{k_1} \\
  ...
\end{pmatrix}$$

By applying this transformation, we get:

 \begin{equation}
 \begin{pmatrix}
 	...\\
 	i_{k2} \\
 	... \\
 	i_{k1} \\
 	...
  \end{pmatrix}
 \ll
 \begin{pmatrix}
 	...\\
 	i'_{k2} \\
 	... \\
 	i'_{k1} \\
 	...
  \end{pmatrix}
 \preceq
  \begin{pmatrix}
 	...\\
 	j_{k2} \\
 	... \\
 	j_{k1} \\
 	...
  \end{pmatrix}
 \ll
 \begin{pmatrix}
 	...\\
 	j'_{k2} \\
 	... \\
 	j'_{k1} \\
 	...
  \end{pmatrix}
 \label{eq:non_interference_iterator_vector_relation}
 \end{equation}

Hence interchange preserves live range non-interference.



% By applying the previous definition of loop interchange on 
% (\ref{eq:non_interference_iterator_vector_relation}), we get :
% \begin{equation*}
% \begin{pmatrix}
% 	...\\
% 	i_{2} \\
% 	... \\
% 	i_{1} \\
% 	...
%  \end{pmatrix}
% \preceq
% \begin{pmatrix}
% 	...\\
% 	i'_{2} \\
% 	... \\
% 	i'_{1} \\
% 	...
%  \end{pmatrix}
% \preceq
%  \begin{pmatrix}
% 	...\\
% 	j_{2} \\
% 	... \\
% 	j_{1} \\
% 	...
%  \end{pmatrix}
% \preceq
% \begin{pmatrix}
% 	... \\
% 	j'_{2} \\
% 	... \\
% 	j'_{1} \\
% 	...
%  \end{pmatrix}
% \label{eq:non_interference_iterator_vector_relation_after_applying_loop_interchange}
% \end{equation*}

% which is true if (\ref{eq:equation_to_be_preserved_after_tiling_2}) is true.
% (\ref{eq:equation_to_be_preserved_after_tiling_2}) is true because 
% (\ref{eq:equation_to_be_preserved_after_tiling}) is true.

% \begin{equation}
% i'_{2} < j_{2} ~ and ~ i'_{1} < j_{1}
% \label{eq:equation_to_be_preserved_after_tiling_2}
% \end{equation}

We can prove that loop skewing also preserves non-interference
in a similar way:
\begin{equation*}
\begin{pmatrix}
	...\\
	i'_{k_1} \\
	... \\
	i'_{k_2} \\
	...
 \end{pmatrix}
\preceq
\begin{pmatrix}
	...\\
	j_{k_1} \\
	... \\
	j_{k_2} \\
	...
 \end{pmatrix}
\implies
\begin{pmatrix}
	...\\
	i'_{k_1}+si'_{k_2} \\
	... \\
	i'_{k_2} \\
	...
 \end{pmatrix}
\preceq
\begin{pmatrix}
	...\\
	j_{k_1}+sj_{k_2} \\
	... \\
	j_{k_2} \\
	...
 \end{pmatrix},~\textrm{with}~s\ge0
\end{equation*}
